Step of Proof: gen_hyp_tp 9,38
Inference at * 1 1 2 
Iof proof for Lemma gen hyp tp:

.....assertion..... NILNIL

1. A : Type
2. e : A
3. H : AType
4. H(e)
5. A  Type
  e  A 
latex
 by ((Thin (-1)) 
CollapseTHEN (AddHiddenLabel `wf`)) 
latex

C1: .....wf..... NILNIL

C1: 4. H(e)
C1:   e  A
C.

origin